the_w:World, e, e':E. FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e') 

latex

Definitions	World, t  T, x:A. B(x), E, FairFifo, P  Q, e <c e', loc(e), Id, s = t, Prop, x:AB(x), P & Q, e <loc e', <a,b>, P  Q, P  Q, sender(e), kind(e), isrcv(k), b, Type, A & B, P  Q, left+right, x:A. B(x), x f y, i=j, x.A(x), x:AB(x), rel_exp(T;R;n), f(a), a<b, {x:A| B(x) }, , , R^+, #$n, time(e)
Lemmas	w-causl-time, rel exp wf, nat plus inc, assert wf, isrcv wf, w-ekind wf, w-sender wf, w-locl wf, Id wf, w-loc wf, w-causl wf, fair-fifo wf, w-E wf, world wf